a:Id, p:FinProbSpace, ds:x:Id fp Type, P:(State(ds)).
(precondition a:Outcome(p) is P:State(ds) -> Bool)  MsgA 

latex

Definitions	type List, IdLnk, t  T, Knd, x.A(x), x:A. B(x), , Id, x:A  B(x), t.2, x:AB(x), Void, rcv(l,tg), KindDeq, f(x)?z, locl(a), Outcome, x : v, t.1, Valtype(da;k), IdDeq, , State(ds), , mk-ma, (precondition a:Outcome(p) is P:State(ds) -> Bool), FinProbSpace, a:A fp B(a), MsgA, Type, x. t(x)
Lemmas	ma-state wf, bool wf, fpf wf, finite-prob-space wf, Id wf, mk-ma wf, locl wf, p-outcome wf, fpf-single wf, rationals wf, id-deq wf, IdLnk wf, ma-valtype wf, pi1 wf, fpf-cap wf, Knd wf, Kind-deq wf, rcv wf, pi2 wf, fpf-empty wf